M:MsgA, l:IdLnk, mss:M.Msg List. withlnk(l;mss)  (tg:IdM.dout(l,tg)) List 

latex

Definitions	MsgA, t  T, IdLnk, x:A. B(x), M.Msg, Id, M.dout(l,tg), withlnk(l;mss), 2of(t), Msg(M), Msg(da), map(f;as), P  Q, mapfilter(f;P;L), mlnk(m), a = b, filter(P;l), b, P & Q, P  Q
Lemmas	assert-eq-lnk, subtype rel self, filter type, map wf, Id wf, ma-dout wf, assert wf, eq lnk wf, ma-msg wf, IdLnk wf, msga wf